\begin{tabbing}
Rinterface($A$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case $A$ of \+
\\[0ex]Rnone =$>$ Rnone()
\\[0ex]Rplus(${\it left}$,${\it right}$)=$>$${\it rec}_{1}$,${\it rec}_{2}$.let $A$\= = ${\it rec}_{1}$ in\+
\\[0ex]let \=$B$\= = ${\it rec}_{2}$ in\+\+
\\[0ex]if\= Rnone?($A$)\+
\\[0ex]then $B$
\-\-\\[0ex]if Rnone?($B$) then $A$ else $A$ $\oplus$ $B$ fi 
\-\-\\[0ex]Rinit(${\it loc}$,$T$,$x$,$v$)=$>$ Rnone()
\\[0ex]Rframe(${\it loc}$,$T$,$x$,$L$)=$>$ Rnone()
\\[0ex]Rsframe(${\it lnk}$,${\it tag}$,$L$)=$>$ Rnone()
\\[0ex]Reffect(${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$f$)=$>$ if isrcv(${\it knd}$)
\\[0ex]then Reffect(${\it loc}$;${\it ds}$;${\it knd}$;$T$;$x$;$f$)
\\[0ex]else Rnone()
\\[0ex]fi 
\\[0ex]Rsends(${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$)=$>$ Rsends(${\it ds}$;${\it knd}$;$T$;$l$;${\it dt}$;$g$)
\\[0ex]Rpre(${\it loc}$,${\it ds}$,$a$,$T$,$P$)=$>$ Rnone()
\\[0ex]Rkframe(${\it loc}$,$k$,$L$)=$>$ Rnone()
\\[0ex]Rksframe(${\it loc}$,$k$,$L$)=$>$ Rnone()
\\[0ex]Rrframe(${\it loc}$,$x$,$L$)=$>$ Rnone()
\-
\end{tabbing}